#include "PDTExpBoolBinNumDerived.h"
#include "PDTCodeGraph.h"
#include "PDTZ3GraphVisitor.h"

PDTLessThan::PDTLessThan(PDTCodeGraph & CG,PDTExpNum &left,PDTExpNum & right)
    : PDTExpBoolBinNum(CG,left,right)
{
}

Z3_ast 
PDTLessThan::Z3NodeVisit (PDTZ3Visitor &ZV)
{
	if (Z3node != NULL) 
		return Z3node;
	
	Z3_ast child1 = getLeft()->Z3visit(ZV);
	Z3_ast child2 = getRight()->Z3visit(ZV);
	
	Z3node = Z3_mk_lt(ZV.ctx,child1,child2);
	return Z3node;
}

PDTGreaterThan::PDTGreaterThan(PDTCodeGraph & CG,PDTExpNum &left,PDTExpNum & right)
  :  PDTExpBoolBinNum(CG,left,right)
{
}


Z3_ast 
PDTGreaterThan::Z3NodeVisit (PDTZ3Visitor &ZV)
{
	if (Z3node != NULL) 
		return Z3node;
	
	Z3_ast child1 = getLeft()->Z3visit(ZV);
	Z3_ast child2 = getRight()->Z3visit(ZV);
	
	Z3node = Z3_mk_gt(ZV.ctx,child1,child2);
	return Z3node;
}

PDTLessThanEqual::PDTLessThanEqual(PDTCodeGraph & CG,PDTExpNum &left,PDTExpNum & right)
  : PDTExpBoolBinNum(CG,left,right)
{
}

Z3_ast 
PDTLessThanEqual::Z3NodeVisit (PDTZ3Visitor &ZV)
{
	if (Z3node != NULL) 
		return Z3node;
	
	Z3_ast child1 = getLeft()->Z3visit(ZV);
	Z3_ast child2 = getRight()->Z3visit(ZV);
	
	Z3node = Z3_mk_le(ZV.ctx,child1,child2);
	return Z3node;
}


PDTGreaterThanEqual::PDTGreaterThanEqual(PDTCodeGraph & CG,PDTExpNum &left,PDTExpNum & right)
    : PDTExpBoolBinNum(CG,left,right)
{
}

Z3_ast 
PDTGreaterThanEqual::Z3NodeVisit (PDTZ3Visitor &ZV)
{
	if (Z3node != NULL) 
		return Z3node;
	
	Z3_ast child1 = getLeft()->Z3visit(ZV);
	Z3_ast child2 = getRight()->Z3visit(ZV);
	
	Z3node = Z3_mk_ge(ZV.ctx,child1,child2);
	return Z3node;
}

PDTEqualNum::PDTEqualNum(PDTCodeGraph & CG,PDTExpNum &left,PDTExpNum & right)
  : PDTExpBoolBinNum(CG,left,right)
{
}

Z3_ast 
PDTEqualNum::Z3NodeVisit (PDTZ3Visitor &ZV)
{
	if (Z3node != NULL) 
		return Z3node;
	
	Z3_ast child1 = getLeft()->Z3visit(ZV);
	Z3_ast child2 = getRight()->Z3visit(ZV);

    assert( Z3_get_sort(ZV.ctx,child1) == Z3_get_sort(ZV.ctx,child2));
    assert( Z3_get_sort(ZV.ctx,child1) == ZV.Int);

    Z3node = Z3_mk_eq(ZV.ctx,child1,child2);
	return Z3node;
}

PDTNotEqualNum::PDTNotEqualNum(PDTCodeGraph & CG,PDTExpNum &left,PDTExpNum & right):PDTExpBoolBinNum(CG,left,right)
{
}




Z3_ast PDTNotEqualNum::Z3NodeVisit (PDTZ3Visitor &ZV){
	if (Z3node != NULL) 
		return Z3node;
	
	Z3_ast child1 = getLeft()->Z3visit(ZV);
	Z3_ast child2 = getRight()->Z3visit(ZV);

    assert( Z3_get_sort(ZV.ctx,child1) == Z3_get_sort(ZV.ctx,child2));
    assert( Z3_get_sort(ZV.ctx,child1) == ZV.Int);

	Z3_ast args[2];
	args[0] = child1;
	args[1] = child2;

    Z3node = Z3_mk_distinct(ZV.ctx,2,args);
    return Z3node;
}
